Skip to content

feat: port algebra/stepindex.v - #515

Merged
Kaptch merged 36 commits into
leanprover-community:masterfrom
ISTA-PLV:StepIndexing
Jul 27, 2026
Merged

feat: port algebra/stepindex.v#515
Kaptch merged 36 commits into
leanprover-community:masterfrom
ISTA-PLV:StepIndexing

Conversation

@alvinylt

@alvinylt alvinylt commented Jul 14, 2026 •
edited
Loading

Copy link
Copy Markdown
Contributor

Description

Port algebra/stepindex.v. It will be nice to have this ready before moving onto algebra/stepindex_finite.v as the latter requires refactoring a large number of files.

Addresses #203.

The current implementation defines SIdx as a type class that extends LT, LE and Zero from Init.Prelude so that we can reuse the notations <, ≤ and 0. Meanwhile, succᵢ is a notation defined on our own.

Checklist of definitions and theorems
  • SIdx.case
  • SIdx.eq_dec
  • SIdx.inhabited
  • SIdx.le_0_l
  • SIdx.le_0_r
  • SIdx.le_dec
  • SIdx.le_gt_cases
  • SIdx.le_lt_trans
  • SIdx.le_lteq (ignored)
  • SIdx.le_neq
  • SIdx.le_ngt
  • SIdx.le_po
  • SIdx.le_succ_diag_r
  • SIdx.le_succ_l
  • SIdx.le_succ_l_2 (ignored)
  • SIdx.le_total
  • SIdx.limit
  • SIdx.limit_0
  • SIdx.limit_S
  • SIdx.limit_finite
  • SIdx.limit_lt_0
  • SIdx.lt_dec
  • SIdx.lt_ge_cases
  • SIdx.lt_le_incl
  • SIdx.lt_le_trans
  • SIdx.lt_nge
  • SIdx.lt_strict
  • SIdx.lt_succ_diag_r (ignored)
  • SIdx.lt_succ_diag_r'
  • SIdx.lt_succ_r
  • SIdx.lt_trans (ignored)
  • SIdx.lt_trichotomy (ignored)
  • SIdx.lt_wf (ignored)
  • SIdx.neq_0_lt_0
  • SIdx.neq_succ_0
  • SIdx.nlt_0_r (ignored)
  • SIdx.nlt_succ_r
  • SIdx.rec
  • SIdx.rec_lim
  • SIdx.rec_lim_ext (ignored)
  • SIdx.rec_succ
  • SIdx.rec_unfold
  • SIdx.rec_zero
  • SIdx.succ_inj
  • SIdx.succ_le_mono
  • SIdx.succ_lt_mono
  • SIdx.succ_neq
  • SIdx.weak_case (ignored)
  • SIdxFinite
  • SIdxMixin
  • sidx

Checklist

  • My code follows the mathlib naming and code style conventions
  • I have added my name to the authors section of any appropriate files

alvinylt added 22 commits July 14, 2026 10:10
@alvinylt
Start porting step-indexing for Transfinite Iris
2db8ec2
@alvinylt
Introduce the type class SIdx
059e3b7
@alvinylt
First theorem for SIdx: nlt_0_r
946c03e
@alvinylt
More Std classes and more SIdx theorems
8debfd2
@alvinylt
More theorem definitions
be0f833
@alvinylt
Four more theorems defined
dabb7e7
@alvinylt
Prove lt_le_trans
60a74ba
@alvinylt
Prove le_lt_trans
2b569f8
@alvinylt
Typo fix
5d88f41
@alvinylt
Prove succ_le_mono, succ_lt_mono
e02680f
@alvinylt
Prove le_0_l, le_0_r
96c333c
@alvinylt
Towards proving more theorems
f436057
@alvinylt
Prove properties about le
f5e0f5a
@alvinylt
More proofs
30096c7
@alvinylt
Even more proofs
904795a
@alvinylt
Further proofs
1aee575
@alvinylt
Prove succ_inj
2ac43a8
@alvinylt
Code reorganisation
b2c2db5
@alvinylt
Remove StepIndexFinite.lean: to be ported later
60232a8
@alvinylt
Add rocq_ignore entries, add decidability instances
cba8474
@alvinylt
Fix rocq_ignore entries, port SIdx.limit
b762bd1
@alvinylt
Port limit_0, limit_lt_0, limit_S, limit_finite
fc7a175
@alvinylt alvinylt mentioned this pull request Jul 15, 2026
Merged
2 tasks
@Kaptch

Kaptch commented Jul 17, 2026

Copy link
Copy Markdown
Collaborator

May I please ask to add in IrisMath instances of SIdx for ordinal type and some initial ordinal (\omega_1 would work)? Most probably non-\omega instances for SIdx would be defined on top of Mathlib, and it would be nice to have examples.

@alvinylt

alvinylt commented Jul 21, 2026

Copy link
Copy Markdown
Contributor Author

May I please ask to add in IrisMath instances of SIdx for ordinal type and some initial ordinal (\omega_1 would work)? Most probably non-\omega instances for SIdx would be defined on top of Mathlib, and it would be nice to have examples.

Two instances of SIdx are introduced, one for Ordinal and another for Subtype with Ordinal.

We have also proved that the notion of limits in SIdx is the same as that for Preorder in Mathlib.

@Kaptch

Kaptch commented Jul 21, 2026

Copy link
Copy Markdown
Collaborator

Thanks!

Kaptch
Kaptch reviewed Jul 21, 2026
View reviewed changes
Comment thread IrisMath/IrisMath/StepIndex.lean
@Kaptch

Kaptch commented Jul 22, 2026

Copy link
Copy Markdown
Collaborator

Nice! I think, unless you want to include something more in this PR, it looks ready to merge.
I'm not sure what plan you have with @MackieLoeffel regarding the subsequent parametrization of OFE/logic with step-index, but if possible, could you please split it into OFE part and logic parts?

@alvinylt

alvinylt commented Jul 22, 2026

Copy link
Copy Markdown
Contributor Author

Given it's likely that Iris/Std/Classes.lean will be removed (#518), I think it will be good to first replace uses of those type classes with built-in ones before merging.

And yes, the plan is to port algebra/stepindex_finite.v after this and parameterise definitions in the algebra folder (following the same PR in Rocq).

but if possible, could you please split it into OFE part and logic parts?

Do you mean separate changes to OFE and CMRA?

@Kaptch

Kaptch commented Jul 22, 2026

Copy link
Copy Markdown
Collaborator

Yep, I think first porting OFE and fixing step-index to \omega on CMRA level; and then porting CMRA fixing step-index in COFESolver would be a good split.
Porting BI is going to require some design choices on how to treat logical rules that don't work in the transfinite logic, and it involves CMRA definition.

In the OFE part, the piece that will need some design choices is Banach fixpoints, because here it would probably be good to think if it makes sense to have two fixpoints: the old one fixed to \omega for people interested in extraction, and step-index fixpoints for people who want to work with transfinite OFEs.

@alvinylt
alvinylt marked this pull request as ready for review July 22, 2026 15:37
@lzy0505 lzy0505 linked an issue Jul 23, 2026 that may be closed by this pull request
Port algebra/stepindex.v #203
Closed
@alvinylt

alvinylt commented Jul 24, 2026

Copy link
Copy Markdown
Contributor Author

Ready to be merged if everything looks good. Then I'll create a separate PR for parametrising OFE.lean on top of this.

@Kaptch

Kaptch commented Jul 24, 2026

Copy link
Copy Markdown
Collaborator

Thank you! Will merge ASAP :)

@Kaptch
Kaptch merged commit 820238b into leanprover-community:master Jul 27, 2026
5 checks passed
@Kaptch

Kaptch commented Jul 27, 2026

Copy link
Copy Markdown
Collaborator

Thanks again! :)
If you start working on adding step-index parameter to OFEs before #533 is merged, please rebase on top of that PR.

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Reviewers

@Kaptch Kaptch Kaptch approved these changes

Assignees

No one assigned

Labels

None yet

Projects

None yet

Milestone

No milestone

Development

Successfully merging this pull request may close these issues.

Port algebra/stepindex.v

2 participants

@alvinylt @Kaptch